
; Copyright (c) 2015 Microsoft Corporation
(get-option :int-real-coercions)

(declare-const x Int)
(declare-fun p (Real) Bool)
(declare-const a (Array Real Bool))
(declare-const b (Array Int Bool))
(declare-const y Real)
(declare-const l1 (List Int))
(declare-const l2 (List Real))
(declare-const q Bool)
(declare-fun f (Int) Bool)

(simplify (p x))
(simplify (select a x))
(simplify (select a q))
(simplify (select b y))
(simplify (store a x true))
(simplify (store b x true))
(simplify (store b y true))
(simplify (insert y l2))
(simplify (+ x y))
(simplify (+ x 1))
(simplify (+ y 1))
(simplify (+ x y 10))
(simplify (< x y))
(display (< x y))
(simplify (/ x y))
(simplify (div x y))
(simplify (f (+ x 1.0)))
